(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun n () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun o () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(assert (not (exists ((l Real)) (= (< 0 h) (or (= (= 0 c) (= (<= 0 l) (= f 2))))))))
(assert (not (exists ((m Real)) (=> (and (or (and (or (and (=> (<= i k) (and (<= 0 (+ (* g i) (- b f))) (<= i (- d)))) (= o j)) (< (+ (+ j (/ (* f (- b f)) 0)) (* (+ (/ g n) 1) (* (* g (/ 1 2)) (/ 0 d)))) o)) (< o j)) (> 0 n)) (<= 0 g) (> 0 d)) (or (< o (* (/ 1 2) (+ (* g (* k k)) (* (* 2 k) (+ b f))))) (< (+ j (/ (- b f) (* 2 (- n)))) o))))))
(assert (= a (+ e i)))
(check-sat)
